Termination w.r.t. Q proof of /tmp/tmpy69P30/thiemann19.trs

Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

1024 → 1024_1(0)
1024_1(x) → if(lt(x, 10), x)
if(true, x) → double(1024_1(s(x)))
if(false, x) → s(0)
lt(0, s(y)) → true
lt(x, 0) → false
lt(s(x), s(y)) → lt(x, y)
double(0) → 0
double(s(x)) → s(s(double(x)))
10 → double(s(double(s(s(0)))))

Q is empty.

↳ QTRS

  ↳ Overlay + Local Confluence

Q restricted rewrite system:
The TRS R consists of the following rules:

1024 → 1024_1(0)
1024_1(x) → if(lt(x, 10), x)
if(true, x) → double(1024_1(s(x)))
if(false, x) → s(0)
lt(0, s(y)) → true
lt(x, 0) → false
lt(s(x), s(y)) → lt(x, y)
double(0) → 0
double(s(x)) → s(s(double(x)))
10 → double(s(double(s(s(0)))))

Q is empty.

The TRS is overlay and locally confluent. By [19] we can switch to innermost.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

1024 → 1024_1(0)
1024_1(x) → if(lt(x, 10), x)
if(true, x) → double(1024_1(s(x)))
if(false, x) → s(0)
lt(0, s(y)) → true
lt(x, 0) → false
lt(s(x), s(y)) → lt(x, y)
double(0) → 0
double(s(x)) → s(s(double(x)))
10 → double(s(double(s(s(0)))))

The set Q consists of the following terms:

1024
1024_1(x0)
if(true, x0)
if(false, x0)
lt(0, s(x0))
lt(x0, 0)
lt(s(x0), s(x1))
double(0)
double(s(x0))
10

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

LT(s(x), s(y)) → LT(x, y)
10¹ → DOUBLE(s(s(0)))
1024_1¹(x) → IF(lt(x, 10), x)
DOUBLE(s(x)) → DOUBLE(x)
IF(true, x) → DOUBLE(1024_1(s(x)))
IF(true, x) → 1024_1¹(s(x))
1024_1¹(x) → LT(x, 10)
10¹ → DOUBLE(s(double(s(s(0)))))
1024_1¹(x) → 10¹
1024¹ → 1024_1¹(0)

The TRS R consists of the following rules:

1024 → 1024_1(0)
1024_1(x) → if(lt(x, 10), x)
if(true, x) → double(1024_1(s(x)))
if(false, x) → s(0)
lt(0, s(y)) → true
lt(x, 0) → false
lt(s(x), s(y)) → lt(x, y)
double(0) → 0
double(s(x)) → s(s(double(x)))
10 → double(s(double(s(s(0)))))

The set Q consists of the following terms:

1024
1024_1(x0)
if(true, x0)
if(false, x0)
lt(0, s(x0))
lt(x0, 0)
lt(s(x0), s(x1))
double(0)
double(s(x0))
10

We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

LT(s(x), s(y)) → LT(x, y)
10¹ → DOUBLE(s(s(0)))
1024_1¹(x) → IF(lt(x, 10), x)
DOUBLE(s(x)) → DOUBLE(x)
IF(true, x) → DOUBLE(1024_1(s(x)))
IF(true, x) → 1024_1¹(s(x))
1024_1¹(x) → LT(x, 10)
10¹ → DOUBLE(s(double(s(s(0)))))
1024_1¹(x) → 10¹
1024¹ → 1024_1¹(0)

The TRS R consists of the following rules:

1024 → 1024_1(0)
1024_1(x) → if(lt(x, 10), x)
if(true, x) → double(1024_1(s(x)))
if(false, x) → s(0)
lt(0, s(y)) → true
lt(x, 0) → false
lt(s(x), s(y)) → lt(x, y)
double(0) → 0
double(s(x)) → s(s(double(x)))
10 → double(s(double(s(s(0)))))

The set Q consists of the following terms:

1024
1024_1(x0)
if(true, x0)
if(false, x0)
lt(0, s(x0))
lt(x0, 0)
lt(s(x0), s(x1))
double(0)
double(s(x0))
10

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 3 SCCs with 6 less nodes.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

                ↳ UsableRulesProof

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

DOUBLE(s(x)) → DOUBLE(x)

The TRS R consists of the following rules:

1024 → 1024_1(0)
1024_1(x) → if(lt(x, 10), x)
if(true, x) → double(1024_1(s(x)))
if(false, x) → s(0)
lt(0, s(y)) → true
lt(x, 0) → false
lt(s(x), s(y)) → lt(x, y)
double(0) → 0
double(s(x)) → s(s(double(x)))
10 → double(s(double(s(s(0)))))

The set Q consists of the following terms:

1024
1024_1(x0)
if(true, x0)
if(false, x0)
lt(0, s(x0))
lt(x0, 0)
lt(s(x0), s(x1))
double(0)
double(s(x0))
10

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

DOUBLE(s(x)) → DOUBLE(x)

R is empty.
The set Q consists of the following terms:

1024
1024_1(x0)
if(true, x0)
if(false, x0)
lt(0, s(x0))
lt(x0, 0)
lt(s(x0), s(x1))
double(0)
double(s(x0))
10

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

1024
1024_1(x0)
if(true, x0)
if(false, x0)
lt(0, s(x0))
lt(x0, 0)
lt(s(x0), s(x1))
double(0)
double(s(x0))
10

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

DOUBLE(s(x)) → DOUBLE(x)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

DOUBLE(s(x)) → DOUBLE(x)
The graph contains the following edges 1 > 1

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

LT(s(x), s(y)) → LT(x, y)

The TRS R consists of the following rules:

1024 → 1024_1(0)
1024_1(x) → if(lt(x, 10), x)
if(true, x) → double(1024_1(s(x)))
if(false, x) → s(0)
lt(0, s(y)) → true
lt(x, 0) → false
lt(s(x), s(y)) → lt(x, y)
double(0) → 0
double(s(x)) → s(s(double(x)))
10 → double(s(double(s(s(0)))))

The set Q consists of the following terms:

1024
1024_1(x0)
if(true, x0)
if(false, x0)
lt(0, s(x0))
lt(x0, 0)
lt(s(x0), s(x1))
double(0)
double(s(x0))
10

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

LT(s(x), s(y)) → LT(x, y)

R is empty.
The set Q consists of the following terms:

1024
1024_1(x0)
if(true, x0)
if(false, x0)
lt(0, s(x0))
lt(x0, 0)
lt(s(x0), s(x1))
double(0)
double(s(x0))
10

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

1024
1024_1(x0)
if(true, x0)
if(false, x0)
lt(0, s(x0))
lt(x0, 0)
lt(s(x0), s(x1))
double(0)
double(s(x0))
10

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

LT(s(x), s(y)) → LT(x, y)

From the DPs we obtained the following set of size-change graphs:

LT(s(x), s(y)) → LT(x, y)
The graph contains the following edges 1 > 1, 2 > 2

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

1024_1¹(x) → IF(lt(x, 10), x)
IF(true, x) → 1024_1¹(s(x))

The TRS R consists of the following rules:

1024 → 1024_1(0)
1024_1(x) → if(lt(x, 10), x)
if(true, x) → double(1024_1(s(x)))
if(false, x) → s(0)
lt(0, s(y)) → true
lt(x, 0) → false
lt(s(x), s(y)) → lt(x, y)
double(0) → 0
double(s(x)) → s(s(double(x)))
10 → double(s(double(s(s(0)))))

The set Q consists of the following terms:

1024
1024_1(x0)
if(true, x0)
if(false, x0)
lt(0, s(x0))
lt(x0, 0)
lt(s(x0), s(x1))
double(0)
double(s(x0))
10

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

Q DP problem:
The TRS P consists of the following rules:

1024_1¹(x) → IF(lt(x, 10), x)
IF(true, x) → 1024_1¹(s(x))

The TRS R consists of the following rules:

10 → double(s(double(s(s(0)))))
lt(0, s(y)) → true
lt(x, 0) → false
lt(s(x), s(y)) → lt(x, y)
double(s(x)) → s(s(double(x)))
double(0) → 0

The set Q consists of the following terms:

1024
1024_1(x0)
if(true, x0)
if(false, x0)
lt(0, s(x0))
lt(x0, 0)
lt(s(x0), s(x1))
double(0)
double(s(x0))
10

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

1024
1024_1(x0)
if(true, x0)
if(false, x0)

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

1024_1¹(x) → IF(lt(x, 10), x)
IF(true, x) → 1024_1¹(s(x))

The TRS R consists of the following rules:

10 → double(s(double(s(s(0)))))
lt(0, s(y)) → true
lt(x, 0) → false
lt(s(x), s(y)) → lt(x, y)
double(s(x)) → s(s(double(x)))
double(0) → 0

The set Q consists of the following terms:

lt(0, s(x0))
lt(x0, 0)
lt(s(x0), s(x1))
double(0)
double(s(x0))
10

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule 1024_1¹(x) → IF(lt(x, 10), x) at position [0,1] we obtained the following new rules:

1024_1¹(x) → IF(lt(x, double(s(double(s(s(0)))))), x)

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

IF(true, x) → 1024_1¹(s(x))
1024_1¹(x) → IF(lt(x, double(s(double(s(s(0)))))), x)

The TRS R consists of the following rules:

10 → double(s(double(s(s(0)))))
lt(0, s(y)) → true
lt(x, 0) → false
lt(s(x), s(y)) → lt(x, y)
double(s(x)) → s(s(double(x)))
double(0) → 0

The set Q consists of the following terms:

lt(0, s(x0))
lt(x0, 0)
lt(s(x0), s(x1))
double(0)
double(s(x0))
10

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ UsableRulesProof

                              ↳ QDP

                                ↳ QReductionProof

Q DP problem:
The TRS P consists of the following rules:

IF(true, x) → 1024_1¹(s(x))
1024_1¹(x) → IF(lt(x, double(s(double(s(s(0)))))), x)

The TRS R consists of the following rules:

double(s(x)) → s(s(double(x)))
lt(0, s(y)) → true
lt(x, 0) → false
lt(s(x), s(y)) → lt(x, y)
double(0) → 0

The set Q consists of the following terms:

lt(0, s(x0))
lt(x0, 0)
lt(s(x0), s(x1))
double(0)
double(s(x0))
10

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

10

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ UsableRulesProof

                              ↳ QDP

                                ↳ QReductionProof

                                  ↳ QDP

                                    ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

IF(true, x) → 1024_1¹(s(x))
1024_1¹(x) → IF(lt(x, double(s(double(s(s(0)))))), x)

The TRS R consists of the following rules:

double(s(x)) → s(s(double(x)))
lt(0, s(y)) → true
lt(x, 0) → false
lt(s(x), s(y)) → lt(x, y)
double(0) → 0

The set Q consists of the following terms:

lt(0, s(x0))
lt(x0, 0)
lt(s(x0), s(x1))
double(0)
double(s(x0))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule 1024_1¹(x) → IF(lt(x, double(s(double(s(s(0)))))), x) at position [0,1] we obtained the following new rules:

1024_1¹(x) → IF(lt(x, s(s(double(double(s(s(0))))))), x)

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ UsableRulesProof

                              ↳ QDP

                                ↳ QReductionProof

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

1024_1¹(x) → IF(lt(x, s(s(double(double(s(s(0))))))), x)
IF(true, x) → 1024_1¹(s(x))

The TRS R consists of the following rules:

double(s(x)) → s(s(double(x)))
lt(0, s(y)) → true
lt(x, 0) → false
lt(s(x), s(y)) → lt(x, y)
double(0) → 0

The set Q consists of the following terms:

lt(0, s(x0))
lt(x0, 0)
lt(s(x0), s(x1))
double(0)
double(s(x0))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule 1024_1¹(x) → IF(lt(x, s(s(double(double(s(s(0))))))), x) at position [0,1,0,0,0] we obtained the following new rules:

1024_1¹(x) → IF(lt(x, s(s(double(s(s(double(s(0)))))))), x)

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ UsableRulesProof

                              ↳ QDP

                                ↳ QReductionProof

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ Rewriting

                                          ↳ QDP

                                            ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

1024_1¹(x) → IF(lt(x, s(s(double(s(s(double(s(0)))))))), x)
IF(true, x) → 1024_1¹(s(x))

The TRS R consists of the following rules:

double(s(x)) → s(s(double(x)))
lt(0, s(y)) → true
lt(x, 0) → false
lt(s(x), s(y)) → lt(x, y)
double(0) → 0

The set Q consists of the following terms:

lt(0, s(x0))
lt(x0, 0)
lt(s(x0), s(x1))
double(0)
double(s(x0))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule 1024_1¹(x) → IF(lt(x, s(s(double(s(s(double(s(0)))))))), x) at position [0,1,0,0] we obtained the following new rules:

1024_1¹(x) → IF(lt(x, s(s(s(s(double(s(double(s(0))))))))), x)

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ UsableRulesProof

                              ↳ QDP

                                ↳ QReductionProof

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ Rewriting

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

1024_1¹(x) → IF(lt(x, s(s(s(s(double(s(double(s(0))))))))), x)
IF(true, x) → 1024_1¹(s(x))

The TRS R consists of the following rules:

double(s(x)) → s(s(double(x)))
lt(0, s(y)) → true
lt(x, 0) → false
lt(s(x), s(y)) → lt(x, y)
double(0) → 0

The set Q consists of the following terms:

lt(0, s(x0))
lt(x0, 0)
lt(s(x0), s(x1))
double(0)
double(s(x0))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule 1024_1¹(x) → IF(lt(x, s(s(s(s(double(s(double(s(0))))))))), x) at position [0,1,0,0,0,0] we obtained the following new rules:

1024_1¹(x) → IF(lt(x, s(s(s(s(s(s(double(double(s(0)))))))))), x)

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ UsableRulesProof

                              ↳ QDP

                                ↳ QReductionProof

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ Rewriting

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

IF(true, x) → 1024_1¹(s(x))
1024_1¹(x) → IF(lt(x, s(s(s(s(s(s(double(double(s(0)))))))))), x)

The TRS R consists of the following rules:

double(s(x)) → s(s(double(x)))
lt(0, s(y)) → true
lt(x, 0) → false
lt(s(x), s(y)) → lt(x, y)
double(0) → 0

The set Q consists of the following terms:

lt(0, s(x0))
lt(x0, 0)
lt(s(x0), s(x1))
double(0)
double(s(x0))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule 1024_1¹(x) → IF(lt(x, s(s(s(s(s(s(double(double(s(0)))))))))), x) at position [0,1,0,0,0,0,0,0,0] we obtained the following new rules:

1024_1¹(x) → IF(lt(x, s(s(s(s(s(s(double(s(s(double(0))))))))))), x)

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ UsableRulesProof

                              ↳ QDP

                                ↳ QReductionProof

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ Rewriting

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

IF(true, x) → 1024_1¹(s(x))
1024_1¹(x) → IF(lt(x, s(s(s(s(s(s(double(s(s(double(0))))))))))), x)

The TRS R consists of the following rules:

double(s(x)) → s(s(double(x)))
lt(0, s(y)) → true
lt(x, 0) → false
lt(s(x), s(y)) → lt(x, y)
double(0) → 0

The set Q consists of the following terms:

lt(0, s(x0))
lt(x0, 0)
lt(s(x0), s(x1))
double(0)
double(s(x0))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule 1024_1¹(x) → IF(lt(x, s(s(s(s(s(s(double(s(s(double(0))))))))))), x) at position [0,1,0,0,0,0,0,0] we obtained the following new rules:

1024_1¹(x) → IF(lt(x, s(s(s(s(s(s(s(s(double(s(double(0)))))))))))), x)

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ UsableRulesProof

                              ↳ QDP

                                ↳ QReductionProof

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ Rewriting

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ Rewriting

                                                          ↳ QDP

                                                            ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

IF(true, x) → 1024_1¹(s(x))
1024_1¹(x) → IF(lt(x, s(s(s(s(s(s(s(s(double(s(double(0)))))))))))), x)

The TRS R consists of the following rules:

double(s(x)) → s(s(double(x)))
lt(0, s(y)) → true
lt(x, 0) → false
lt(s(x), s(y)) → lt(x, y)
double(0) → 0

The set Q consists of the following terms:

lt(0, s(x0))
lt(x0, 0)
lt(s(x0), s(x1))
double(0)
double(s(x0))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule 1024_1¹(x) → IF(lt(x, s(s(s(s(s(s(s(s(double(s(double(0)))))))))))), x) at position [0,1,0,0,0,0,0,0,0,0] we obtained the following new rules:

1024_1¹(x) → IF(lt(x, s(s(s(s(s(s(s(s(s(s(double(double(0))))))))))))), x)

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ UsableRulesProof

                              ↳ QDP

                                ↳ QReductionProof

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ Rewriting

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ Rewriting

                                                          ↳ QDP

                                                            ↳ Rewriting

                                                              ↳ QDP

                                                                ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

1024_1¹(x) → IF(lt(x, s(s(s(s(s(s(s(s(s(s(double(double(0))))))))))))), x)
IF(true, x) → 1024_1¹(s(x))

The TRS R consists of the following rules:

double(s(x)) → s(s(double(x)))
lt(0, s(y)) → true
lt(x, 0) → false
lt(s(x), s(y)) → lt(x, y)
double(0) → 0

The set Q consists of the following terms:

lt(0, s(x0))
lt(x0, 0)
lt(s(x0), s(x1))
double(0)
double(s(x0))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule 1024_1¹(x) → IF(lt(x, s(s(s(s(s(s(s(s(s(s(double(double(0))))))))))))), x) at position [0,1,0,0,0,0,0,0,0,0,0,0,0] we obtained the following new rules:

1024_1¹(x) → IF(lt(x, s(s(s(s(s(s(s(s(s(s(double(0)))))))))))), x)

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ UsableRulesProof

                              ↳ QDP

                                ↳ QReductionProof

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ Rewriting

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ Rewriting

                                                          ↳ QDP

                                                            ↳ Rewriting

                                                              ↳ QDP

                                                                ↳ Rewriting

                                                                  ↳ QDP

                                                                    ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

IF(true, x) → 1024_1¹(s(x))
1024_1¹(x) → IF(lt(x, s(s(s(s(s(s(s(s(s(s(double(0)))))))))))), x)

The TRS R consists of the following rules:

double(s(x)) → s(s(double(x)))
lt(0, s(y)) → true
lt(x, 0) → false
lt(s(x), s(y)) → lt(x, y)
double(0) → 0

The set Q consists of the following terms:

lt(0, s(x0))
lt(x0, 0)
lt(s(x0), s(x1))
double(0)
double(s(x0))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ UsableRulesProof

                              ↳ QDP

                                ↳ QReductionProof

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ Rewriting

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ Rewriting

                                                          ↳ QDP

                                                            ↳ Rewriting

                                                              ↳ QDP

                                                                ↳ Rewriting

                                                                  ↳ QDP

                                                                    ↳ UsableRulesProof

                                                                      ↳ QDP

                                                                        ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

IF(true, x) → 1024_1¹(s(x))
1024_1¹(x) → IF(lt(x, s(s(s(s(s(s(s(s(s(s(double(0)))))))))))), x)

The TRS R consists of the following rules:

double(0) → 0
lt(0, s(y)) → true
lt(s(x), s(y)) → lt(x, y)
lt(x, 0) → false

The set Q consists of the following terms:

lt(0, s(x0))
lt(x0, 0)
lt(s(x0), s(x1))
double(0)
double(s(x0))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule 1024_1¹(x) → IF(lt(x, s(s(s(s(s(s(s(s(s(s(double(0)))))))))))), x) at position [0,1,0,0,0,0,0,0,0,0,0,0] we obtained the following new rules:

1024_1¹(x) → IF(lt(x, s(s(s(s(s(s(s(s(s(s(0))))))))))), x)

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ UsableRulesProof

                              ↳ QDP

                                ↳ QReductionProof

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ Rewriting

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ Rewriting

                                                          ↳ QDP

                                                            ↳ Rewriting

                                                              ↳ QDP

                                                                ↳ Rewriting

                                                                  ↳ QDP

                                                                    ↳ UsableRulesProof

                                                                      ↳ QDP

                                                                        ↳ Rewriting

                                                                          ↳ QDP

                                                                            ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

IF(true, x) → 1024_1¹(s(x))
1024_1¹(x) → IF(lt(x, s(s(s(s(s(s(s(s(s(s(0))))))))))), x)

The TRS R consists of the following rules:

double(0) → 0
lt(0, s(y)) → true
lt(s(x), s(y)) → lt(x, y)
lt(x, 0) → false

The set Q consists of the following terms:

lt(0, s(x0))
lt(x0, 0)
lt(s(x0), s(x1))
double(0)
double(s(x0))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ UsableRulesProof

                              ↳ QDP

                                ↳ QReductionProof

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ Rewriting

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ Rewriting

                                                          ↳ QDP

                                                            ↳ Rewriting

                                                              ↳ QDP

                                                                ↳ Rewriting

                                                                  ↳ QDP

                                                                    ↳ UsableRulesProof

                                                                      ↳ QDP

                                                                        ↳ Rewriting

                                                                          ↳ QDP

                                                                            ↳ UsableRulesProof

                                                                              ↳ QDP

                                                                                ↳ QReductionProof

Q DP problem:
The TRS P consists of the following rules:

IF(true, x) → 1024_1¹(s(x))
1024_1¹(x) → IF(lt(x, s(s(s(s(s(s(s(s(s(s(0))))))))))), x)

The TRS R consists of the following rules:

lt(0, s(y)) → true
lt(s(x), s(y)) → lt(x, y)
lt(x, 0) → false

The set Q consists of the following terms:

lt(0, s(x0))
lt(x0, 0)
lt(s(x0), s(x1))
double(0)
double(s(x0))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

double(0)
double(s(x0))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ UsableRulesProof

                              ↳ QDP

                                ↳ QReductionProof

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ Rewriting

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ Rewriting

                                                          ↳ QDP

                                                            ↳ Rewriting

                                                              ↳ QDP

                                                                ↳ Rewriting

                                                                  ↳ QDP

                                                                    ↳ UsableRulesProof

                                                                      ↳ QDP

                                                                        ↳ Rewriting

                                                                          ↳ QDP

                                                                            ↳ UsableRulesProof

                                                                              ↳ QDP

                                                                                ↳ QReductionProof

                                                                                  ↳ QDP

                                                                                    ↳ RemovalProof

Q DP problem:
The TRS P consists of the following rules:

IF(true, x) → 1024_1¹(s(x))
1024_1¹(x) → IF(lt(x, s(s(s(s(s(s(s(s(s(s(0))))))))))), x)

The TRS R consists of the following rules:

lt(0, s(y)) → true
lt(s(x), s(y)) → lt(x, y)
lt(x, 0) → false

The set Q consists of the following terms:

lt(0, s(x0))
lt(x0, 0)
lt(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
In the following pairs the term without variables s(s(s(s(s(s(s(s(s(s(0)))))))))) is replaced by the fresh variable x_removed.
Pair: 1024_1¹(x) → IF(lt(x, s(s(s(s(s(s(s(s(s(s(0))))))))))), x)
Positions in right side of the pair:

[0,1]

The new variable was added to all pairs as a new argument[13].

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ UsableRulesProof

                              ↳ QDP

                                ↳ QReductionProof

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ Rewriting

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ Rewriting

                                                          ↳ QDP

                                                            ↳ Rewriting

                                                              ↳ QDP

                                                                ↳ Rewriting

                                                                  ↳ QDP

                                                                    ↳ UsableRulesProof

                                                                      ↳ QDP

                                                                        ↳ Rewriting

                                                                          ↳ QDP

                                                                            ↳ UsableRulesProof

                                                                              ↳ QDP

                                                                                ↳ QReductionProof

                                                                                  ↳ QDP

                                                                                    ↳ RemovalProof

                                                                                      ↳ QDP

                                                                                        ↳ NonInfProof

Q DP problem:
The TRS P consists of the following rules:

1024_1¹(x, x_removed) → IF(lt(x, x_removed), x, x_removed)
IF(true, x, x_removed) → 1024_1¹(s(x), x_removed)

The TRS R consists of the following rules:

lt(0, s(y)) → true
lt(s(x), s(y)) → lt(x, y)
lt(x, 0) → false

The set Q consists of the following terms:

lt(0, s(x0))
lt(x0, 0)
lt(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
The DP Problem is simplified using the Induction Calculus [18] with the following steps:
Note that final constraints are written in bold face.

For Pair IF(true, x, x_removed) → 1024_1¹(s(x), x_removed) the following chains were created:

We consider the chain 1024_1¹(x, x_removed) → IF(lt(x, x_removed), x, x_removed), IF(true, x, x_removed) → 1024_1¹(s(x), x_removed) which results in the following constraint:
(1)    (IF(lt(x2, x3), x2, x3)=IF(true, x4, x5) ⇒ IF(true, x4, x5)≥1024_1¹(s(x4), x5))

We simplified constraint (1) using rules (I), (II), (III) which results in the following new constraint:
(2)    (lt(x2, x3)=true ⇒ IF(true, x2, x3)≥1024_1¹(s(x2), x3))

We simplified constraint (2) using rule (V) (with possible (I) afterwards) using induction on lt(x2, x3)=true which results in the following new constraints:
(3)    (true=true ⇒ IF(true, 0, s(x12))≥1024_1¹(s(0), s(x12)))

(4)    (lt(x13, x14)=true∧(lt(x13, x14)=true ⇒ IF(true, x13, x14)≥1024_1¹(s(x13), x14)) ⇒ IF(true, s(x13), s(x14))≥1024_1¹(s(s(x13)), s(x14)))

We simplified constraint (3) using rules (I), (II) which results in the following new constraint:
(5)    (IF(true, 0, s(x12))≥1024_1¹(s(0), s(x12)))

We simplified constraint (4) using rule (VI) where we applied the induction hypothesis (lt(x13, x14)=true ⇒ IF(true, x13, x14)≥1024_1¹(s(x13), x14)) with σ = [ ] which results in the following new constraint:
(6)    (IF(true, x13, x14)≥1024_1¹(s(x13), x14) ⇒ IF(true, s(x13), s(x14))≥1024_1¹(s(s(x13)), s(x14)))

For Pair 1024_1¹(x, x_removed) → IF(lt(x, x_removed), x, x_removed) the following chains were created:

We consider the chain IF(true, x, x_removed) → 1024_1¹(s(x), x_removed), 1024_1¹(x, x_removed) → IF(lt(x, x_removed), x, x_removed) which results in the following constraint:
(7) (1024_1¹(s(x6), x7)=1024_1¹(x8, x9) ⇒ 1024_1¹(x8, x9)≥IF(lt(x8, x9), x8, x9))

We simplified constraint (7) using rules (I), (II), (III) which results in the following new constraint:
(8) (1024_1¹(s(x6), x7)≥IF(lt(s(x6), x7), s(x6), x7))

To summarize, we get the following constraints P_≥ for the following pairs.

IF(true, x, x_removed) → 1024_1¹(s(x), x_removed)
- (IF(true, 0, s(x12))≥1024_1¹(s(0), s(x12)))
- (IF(true, x13, x14)≥1024_1¹(s(x13), x14) ⇒ IF(true, s(x13), s(x14))≥1024_1¹(s(s(x13)), s(x14)))
1024_1¹(x, x_removed) → IF(lt(x, x_removed), x, x_removed)
- (1024_1¹(s(x6), x7)≥IF(lt(s(x6), x7), s(x6), x7))

The constraints for P_> respective P_bound are constructed from P_≥ where we just replace every occurence of "t ≥ s" in P_≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for P_bound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation [18]:

POL(0) = 0
POL(1024_1¹(x₁, x₂)) = -1 - x₁ + x₂
POL(IF(x₁, x₂, x₃)) = -1 - x₂ + x₃
POL(c) = -2
POL(false) = 0
POL(lt(x₁, x₂)) = 0
POL(s(x₁)) = 1 + x₁
POL(true) = 1

The following pairs are in P_>:

IF(true, x, x_removed) → 1024_1¹(s(x), x_removed)

The following pairs are in P_bound:

IF(true, x, x_removed) → 1024_1¹(s(x), x_removed)

There are no usable rules

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ UsableRulesProof

                              ↳ QDP

                                ↳ QReductionProof

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ Rewriting

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ Rewriting

                                                          ↳ QDP

                                                            ↳ Rewriting

                                                              ↳ QDP

                                                                ↳ Rewriting

                                                                  ↳ QDP

                                                                    ↳ UsableRulesProof

                                                                      ↳ QDP

                                                                        ↳ Rewriting

                                                                          ↳ QDP

                                                                            ↳ UsableRulesProof

                                                                              ↳ QDP

                                                                                ↳ QReductionProof

                                                                                  ↳ QDP

                                                                                    ↳ RemovalProof

                                                                                      ↳ QDP

                                                                                        ↳ NonInfProof

                                                                                          ↳ QDP

                                                                                            ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

1024_1¹(x, x_removed) → IF(lt(x, x_removed), x, x_removed)

The TRS R consists of the following rules:

lt(0, s(y)) → true
lt(s(x), s(y)) → lt(x, y)
lt(x, 0) → false

The set Q consists of the following terms:

lt(0, s(x0))
lt(x0, 0)
lt(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 0 SCCs with 1 less node.